;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
; The code for this module was adapted for ACL2 from a 
; bitmap resize algorithm and source code found on the 
; website http://www.davdata.nl/math/bmresize.html.
; The algorithm goes through the following steps:
; 1) scan destination bitmap bm2 , row by row
; 2) for each pixel in bm2, calculate overlap with source 
;    bitmap bm1
; 3) scan all pixels in source which are overlapped
; 4) add colors of these pixels according to fraction of 
;    overlap
; 5) copy color to destination pixel
(require "mbmptree.lisp")
(require "iresize.lisp")

(module Mresize
  (import Ibmptree)
  ; Returns the new width of the pixel for calculating the
  ; the amount of horizontal overlap for each pixel.
  ; pre: dx - a rational number
  ;      i - the row of the old pixel
  ;      sx1 - the distance from the left edge of the area covered
  ;            by the new pixel to the left edge of the map
  ;      sx2 - the distance from the right edge of the area covered
  ;            by the new pixel to the left edge of the map
  ; post: an integer equal to the calculated length of
  ;       the horizontal edge of the area in the original bitmap
  ;       covered by the pixel in the new bitmap 
  (defun get-new-dx (dx i sx1 sx2)
    (if (> sx1 i)
        (if (< sx2 (+ i 1))
            (- (- dx (- sx1 i)) (- (+ i 1) sx2))
            (- dx (- sx1 i)))
        (if (< sx2 (+ i 1))
            (- dx (- (+ i 1) sx2))
            dx)))

  ; Returns the new height of the pixel for calculating the
  ; the amount of vertical overlap for each pixel.
  ; pre: dy - a rational number
  ;      j - the column of the old pixel
  ;      sy1 - the distance from the top of the area covered
  ;            by the new pixel to the top of the map
  ;      sy2 - the distance from the bottom of the area covered
  ;            by the new pixel to the top of the map
  ; post: an integer equal to the calculated length of
  ;       the vertical edge of the area in the original bitmap
  ;       covered by the pixel in the new bitmap
  (defun get-new-dy (dy j sy1 sy2)
    (if (> sy1 j)
        (if (< sy2 (+ j 1))
            (- (- dy (- sy1 j)) (- (+ j 1) sy2))
            (- dy (- sy1 j)))
        (if (< sy2 (+ j 1))
            (- dy (- (+ j 1) sy2))
            dy)))

  ; Scans all of the pixels in the original bitmap that are 
  ; overlapped horizontally by pixels in the resized bitmap and
  ; combines those colors proportionally to the area in each
  ; covered by the new pixel to calculate the color values for
  ; the new pixel in the new bitmap.
  ; pre: oldtree - bmp-tree representation of the original
  ;                bitmap
  ;      oldRow - the row-list at the current row in the original
  ;               bmp-tree
  ;      col - column of the current pixel to check
  ;      row - row of the current pixel to check
  ;      sx1 - the distance from the left edge of the area covered
  ;            by the new pixel to the left edge of the map
  ;      sx2 - the distance from the right edge of the area covered
  ;            by the new pixel to the left edge of the map
  ;      fi2 - the inverse of the square of the ratio of the width 
  ;            of the original bitmap to the width of the resized
  ;            bitmap
  ;      dy - an integer equal to the calculated length of
  ;           the vertical edge of the area in the original bitmap
  ;           covered by the pixel in the new bitmap
  ;      destR, destG, destB - the color (RGB) values for the 
  ;                            new pixel in the resized bitmap
  ; post: a list of nontruncated RGB color values for the new 
  ;       pixel in the resized bitmap
  (defun scan-horizontal-overlap (oldTree oldRow col row sx1 sx2 fi2
                                          dy destR destG destB)
    (if (< col (ceiling sx2 1))
        (let* ((newdx (get-new-dx 1 col sx1 sx2))
               ; get the color of the corresponding pixel in the 
               ; original bitmap
               (colors (cdar oldRow))
               ; pull out each color byte
               (sR (car colors))
               (sG (cadr colors))
               (sB (caddr colors))
               ; get the fraction of the new pixel that overlaps
               ; pixel (i, j) in the original bitmap
               (PC (* newdx (* dy fi2)))
               ; calculate the new color bytes
               (newdestR (+ destR (* sR PC)))
               (newdestG (+ destG (* sG PC)))
               (newdestB (+ destB (* sB PC))))
          ; calculate the new colors for the next pixel in the row
          (scan-horizontal-overlap oldTree (cdr oldRow) (+ col 1) 
                                   row sx1 sx2 fi2 dy newdestR 
                                   newdestG newdestB))
        (list destR destG destB)))
  
  ; Scans all of the pixels in the original bitmap that are 
  ; overlapped vertically by pixels in the resized bitmap and
  ; combines those colors proportionally to the area in each
  ; covered by the new pixel to calculate the color values for
  ; the new pixel in the new bitmap.
  ; pre: oldtree - bmp-tree representation of the original
  ;                bitmap
  ;      row - row of the current pixel to check
  ;      sy1 - the distance from the top of the area covered
  ;            by the new pixel to the top of the map
  ;      sy2 - the distance from the bottom of the area covered
  ;            by the new pixel to the top of the map
  ;      sx1 - the distance from the left edge of the area covered
  ;            by the new pixel to the left edge of the map
  ;      sx2 - the distance from the right edge of the area covered
  ;            by the new pixel to the left edge of the map
  ;      fi2 - the inverse of the square of the ratio of the width 
  ;            of the original bitmap to the width of the resized
  ;            bitmap
  ;      destR, destG, destB - the color (RGB) values for the 
  ;                            new pixel in the resized bitmap
  ; post: a list of RGB color values for the new pixel in the 
  ;       resized bitmap
  (defun scan-vertical-overlap (oldTree row sy1 sy2 sx1 sx2 fi2 destR 
                                        destG destB)
    (if (< row (ceiling sy2 1))
        (let* ((newdy (get-new-dy 1 row sy1 sy2))
               (startCol (floor sx1 1))
               (oldRow (nthcdr startCol (get-row oldTree row)))
               (colors (scan-horizontal-overlap oldTree oldRow
                                                startCol row
                                                sx1 sx2 fi2 
                                                newdy destR 
                                                destG destB))
               (newdestR (car colors))
               (newdestG (cadr colors))
               (newdestB (caddr colors)))
          (scan-vertical-overlap oldTree (+ row 1) sy1 sy2 sx1 sx2 
                                 fi2 newdestR newdestG newdestB))
        (list (truncate destR 1) (truncate destG 1) 
              (truncate destB 1))))
  
  ; Adds the new pixels in each column of a row in the resized 
  ; bitmap.
  ; pre: oldtree - bmp-tree representation of the original
  ;                bitmap
  ;      col - the column of the new pixel
  ;      row - the row of the new pixel
  ;      destWidth - the width of the resized image
  ;      sy1 - the distance from the top of the area covered
  ;            by the new pixel to the top of the map
  ;      sy2 - the distance from the bottom of the area covered
  ;            by the new pixel to the top of the map
  ;      f - the ratio of the width of the original bitmap to
  ;          the width of the resized bitmap
  ;      fi2 - the inverse of the square of the ratio of the width 
  ;            of the original bitmap to the width of the resized
  ;            bitmap
  ; post: the new row to be added to the resized bmp-tree
  (defun set-horizontal-destination-pixels (oldTree col row 
                                                    destWidth 
                                                    sy1 sy2 f fi2)
    (if (< col destWidth)
        (let* ((sx1 (* f col))
               (sx2 (+ sx1 f))
               (colors (scan-vertical-overlap oldTree (floor sy1 1) 
                                              sy1 sy2 sx1 sx2 fi2 
                                              0 0 0))
               ; create the new pixel
               (pixel (cons col colors)))
          ; add the new pixel to the resized row list
          (cons pixel 
                (set-horizontal-destination-pixels 
                 oldTree (+ col 1) row destWidth
                 sy1 sy2 f fi2)))
        nil))

  ; Adds each row of pixels to the resized bitmap.
  ; pre: oldtree - bmp-tree representation of the original
  ;                bitmap
  ;      newTree - the tree-representation of the new bitmap
  ;      row - the row of the new pixel
  ;      destHeight - the height of the resized image
  ;      destWidth - the width of the resized image
  ;      f - the ratio of the width of the original bitmap to
  ;          the width of the resized bitmap
  ;      fi2 - the inverse of the square of the ratio of the width 
  ;            of the original bitmap to the width of the resized
  ;            bitmap
  ; post: the tree-representation of the resized bitmap
  (defun set-vertical-destination-pixels (oldTree newTree row 
                                                  destHeight 
                                                  destWidth f fi2)
    (if (< row destHeight)
        (let* ((sy1 (* f row))
               (sy2 (+ sy1 f))
               ; resize the current row
               (newRow 
                (set-horizontal-destination-pixels oldTree 0
                                                   row destWidth 
                                                   sy1 sy2 f fi2)))
          ; insert the resized row into the tree and resize the
          ; next row
          (set-vertical-destination-pixels 
           oldTree (insert-row newTree row newRow)
           (+ row 1) destHeight destWidth f fi2))
        newTree))
  
  ; Resizes the bitmap to the given percentage of the original
  ; bitmap.
  ; pre: tr - tree representation of the original bitmap
  ;      perc - integer percentage of the new bitmap compared
  ;             to the original bitmap
  ; post: a resized bmp-tree
  (defun resize (tr perc)
    (if (and (bmp-tree? tr) (natp perc))
        (let* ((dimensions (get-dimensions tr))
               (header (get-header tr))
               (sh (car dimensions))
               (sw (cdr dimensions))
               (destWidth (truncate (* sw (/ perc 100)) 1))
               (f (/ sw destWidth))
               (fi (/ 1 f))
               (fi2 (* fi fi))
               (destHeight (truncate (/ sh f) 1))
               (newTree 
                (insert-header 
                 (set-vertical-destination-pixels tr 
                                                  (empty-bmp-tree) 
                                                  0 destHeight 
                                                  destWidth f fi2)
                 header))
               (newDim (get-dimensions newTree)))
          (set-dimensions-header newTree (car newDim) (cdr newDim)))      
        tr))
  (export Iresize))
